#include "Results.cuh"

Results::Results(int number_of_vars, bool on_gpu)
{

	this->on_gpu = on_gpu;
	this->number_of_vars = number_of_vars;

	if(on_gpu)
	{
		check(cudaMalloc(&results_dev, sizeof(sat_status)*number_of_vars), "Allocating results on GPU");
		check(cudaMalloc(&formula_status_dev, sizeof(sat_status)), "Allocating results on GPU");

		sat_status undef_stat = UNDEF;
		sat_status unsat_stat = UNSAT;

		check(cudaMemcpy(formula_status_dev, &unsat_stat, sizeof(sat_status), cudaMemcpyHostToDevice), "Copying results to GPU");

		for(int i = 0; i < number_of_vars; i++)
			check(cudaMemcpy(results_dev+i, &undef_stat, sizeof(sat_status), cudaMemcpyHostToDevice), "Copying results to GPU");
	}
	else
		formula_status_host = UNSAT;



}

__device__ void Results::set_satisfiable_results(Lit* the_results, int size)
{
	assert(on_gpu);

	*formula_status_dev = SAT;

	for(int i = 0; i < size; i++)
	{
		Lit l = the_results[i];
		int index = var(l);

#ifdef USE_ASSERTIONS
		assert(index >= 0);
#endif

		sat_status res_sign = sign(l) ? SAT : UNSAT;

		results_dev[index] = res_sign;
	}
}

__host__ __device__ void Results::set_undef()
{
#ifndef __CUDA_ARCH__
	assert(!on_gpu);
	formula_status_host = UNDEF;
#else
	assert(on_gpu);
	*formula_status_dev = UNDEF;
#endif
}
__host__ void Results::set_host_status(sat_status status)
{
	assert(!on_gpu);
	formula_status_host = status;
}

__host__ void Results::print_results(vector <Lit> & set_literals)
{
	sat_status status;

	if(on_gpu)
	{
		check(cudaMemcpy(&status, formula_status_dev, sizeof(sat_status), cudaMemcpyDeviceToHost), "Copying results from GPU");
	}
	else
	{
		status = formula_status_host;
	}

	switch(status)
	{
	case UNDEF:
		printf("UNDEF\n");
		break;
	case UNSAT:
		printf("UNSAT\n");
		break;
	case SAT:
		print_sat_results(set_literals);
		printf("SAT\n");
		break;
	default:
		assert(false);
		break;

	}

}
__host__ sat_status Results::get_status()
{
	sat_status status;
	if(on_gpu)
		check(cudaMemcpy(&status, formula_status_dev, sizeof(sat_status), cudaMemcpyDeviceToHost), "Copying results from GPU");
	else
		status = formula_status_host;

	return status;
}

__host__ void Results::print_sat_results(vector <Lit> & set_literals)
{

	sat_status * results_host = (sat_status*)malloc(sizeof(sat_status)*number_of_vars);
	if(on_gpu)
		check(cudaMemcpy(results_host, results_dev, sizeof(sat_status)*number_of_vars, cudaMemcpyDeviceToHost), "Copying results from GPU");
	else
	{
		for(int i = 0; i < number_of_vars; i++)
			results_host[i] = UNDEF;
	}

	for(std::vector<Lit>::iterator it = set_literals.begin(); it != set_literals.end(); ++it)
	{
		int index = var(*it);
		sat_status stat = sign(*it) ? SAT : UNSAT;
		results_host[index] = stat;
	}

	for(int i = 0; i < number_of_vars; i++)
	{
		if(results_host[i] == SAT || results_host[i] == UNDEF)
		{
			printf("%d ", i+1);
		}
		else
		{
			if(results_host[i] == UNSAT)
			printf("-%d ", i+1);
		}
	}

	printf("0\n");


	free(results_host);
}
